r,s,t:rationals. ((r + s) + t) = (r + (s + t))  rationals 

latex

Definitions	ff, tt, qinv(r), r * s, if b then t else f fi , qdiv(r; s), P  Q, P  Q, qeq(r; s), P  Q, r + s, t  T, x:A. B(x), False, nequal(T; a; b), A, A c B, int_nzero, x:A. B(x), P  Q, prop{i:l}
Lemmas	qeq wf2, assert wf, assert of eq int, int nzero properties, q-elim, qadd wf, assert-qeq, rationals wf